With braiding
With duals for objects
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
With duals for morphisms
monoidal dagger-category?
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
In higher category theory
In the strict sense of the word, a cartesian product is a product in Set, the category of sets. Hence for and two sets, their cartesian product is the set denoted whose elements are ordered pairs of elements in and , respectively.
The abstract concept of such products generalizes from Set to any other category (as a special case of a category-theoretic limit), only that in general products of any given objects may or may not actually exist in that category.
(If they all exist, then one speaks of a cartesian monoidal category. Especially if the category is also a monoidal category with respect to some other tensor product, then one says “Cartesian product” to distinguish the two. For instance one speaks of the cartesian product on Cat and on 2Cat in contrast to the Gray tensor product.)
A product created by the forgetful functor of a concrete category, especially in algebra, is often called a direct product (for instance a direct product of groups).
Given any family of sets, the cartesian product of the family is the set of all functions from the index set with in for each in .
As stated, the target of such a function depends on the argument, which is natural in dependent type theory; but if you don’t like this, then define to be the set of those functions from to the disjoint union such that (treating as a subset of as usual) for each in .
In traditional forms of set theory, one can also take the target of to be the union or even the class of all objects (equivalently, leave it unspecified).
Given any category , and any set of its objects, then the product of all these objects is, if it exists, an object denoted
and equipped with morphisms
(the projections), for each , such that it is universal with this property, i.e. such that given any other object with morphisms
for , then there is a unique morphism
which factors the through the , i.e. such that all these diagrams commute:
for all .
In the case of a binary product it is also denoted by “”:
An important special case is a power of an object , where (referring to notation above) we take all to be and form
Referring to notation above, if we take and all to be the identity morphism , then the map
is called the diagonal morphism, typically denoted by or . For example, we have a diagonal map
for binary products.
If a category admits -fold products (products over an indexing set ), then a product functor
can be defined, taking a collection of objects to their product, and taking a collection of morphisms to a morphism
defined to be , using the notation above. (N.B.: the category of (small) categories has itself small products, and the notation makes reference to this fact. With some care, we can remove the restriction to small categories.)
As a functor, is right adjoint to the diagonal functor . The unit of the adjunction , at the component , is the diagonal morphism
and the counit is the -tuple of projection maps:
Following the yoga of adjunctions, we can write the “tupling” in terms of the product functor and the unit/diagonal map:
while in the other direction, as stated in the universal property above, we can retrieve the components of a general map in terms of the diagonal functor and the counit/projection maps. It boils down to saying
Given sets and , the cartesian product of the binary family is written ; its elements are called ordered pairs. (In set theory, one often makes a special definition for this case, defining
rather than as a function so that ordered pairs can then be used in the definition of function. From a structural perspective, however, this is unnecessary.)
Given sets through , the cartesian product of the -ary family is written ; its elements are called ordered -tuples.
Given sets , , etc, the cartesian product of the countably infinitary family is written ; its elements are called infinite sequences.
Given a set , the cartesian product of the unary family may be identified with itself; that is, we identify the ordered singleton with .
The cartesian product of the empty family is the point, a set whose only element is the empty list ; we often call this set (or , when we're Urs) and write its element as .
For algebraic categories like Grp, where the objects are sets equipped with (globally defined) specified operations that satisfy specified universally quantified identities, products are always constructed in the way you’d expect, viz. by taking products at the level of the underlying sets and endowing them with operations defined in the evident pointwise fashion, just like the way it works in . More commentary on this in more general contexts will be given below.
For a non-example: The category Field of fields does not admit products, even though some might consider that an algebraic example (in some loose or informal sense).
In categories of topological type, products are again constructed in a common sense manner; see for instance product topological space for a prototype.
For topological categories, which include examples like Top and Preord, products (e.g. product topological spaces) are always constructed in the way one expects, by taking products at the level of the underlying sets and endowing them with an initial lift structure; e.g., in the case of , the smallest or initial topology for which the projection maps are continuous.
This principle continues to hold even for infinitary products, where the correct structure might not be obvious without guidance from categorical considerations. For example, for topological spaces, for an infinite product , we use the product topology, and not say the box topology which might be the first thing one would try.
In any presheaf category, i.e., a category of type where is a small category, products are calculated in obvious pointwise fashion, where with the pointwise product projection maps. This even works if is large (making ‘very large’).
If has products and is a reflective subcategory, products in exist and are calculated as they are in . For example, this applies to any Grothendieck topos, as a category of sheaves on a site forming a reflective subcategory of a category of presheaves (on the underlying category of the site).
Generalizing the last example still further, if is a monadic functor, then products and more generally limits in are created (or reflected) from products/limits in . In other words, products of algebras over a monad are given by products in , equipped with the evident “pointwise” -algebra structure.
If has products and is a coreflective subcategory, where has a right adjoint (co-reflector) , then products in can be formed by taking products in and then applying .
Products in are given by coproducts in .
In some cases, this formal tautology gives the only sensible way to construct products. For example, to form products in the category Loc of locales, one must take the formal dual of the coproduct (denoted ) in the category of frames.
Similarly, the product of two affine schemes is the formal dual of the coproduct of their corresponding coordinate rings, again given by a tensor product.
Relative to a symmetric monoidal category with monoidal product , products in the category of cocommutative comonoids are given by the tensor product in the underlying smc category.
For categories enriched in the category of commutative monoids, finite products are biproducts and hence coincide with coproducts in a controlled fashion (via matrices). However, this is usually not the case for infinite products. For such examples, finite products are absolute limits.
In the category SupLat of sup-lattices, arbitrary products coincide with coproducts (and in fact the functor that takes a sup-lattice to its posetal opposite is part of a perfect duality , taking a sup-lattice map to where ). This example descends to itself, so we conclude that products in are actually given by coproducts in which in turn are given by coproducts in .
In the Cat the cartesian product is the product of categories.
If either projection out of a Cartesian product is regarded as a (fiber) bundle map, it is called a trivial fiber bundle.
Under the relation between category theory and type theory products in a category correspond to product types in type theory.
type theory | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
product type | product | |
type formation | ||
term introduction | ||
term elimination | ||
computation rule |
In material set theory, the existence of binary cartesian products follows from the axiom of pairing and the axiom of weak replacement? (which is very weak). In structural set theory, their existence generally must be stated as an axiom: the axiom of products. See ordered pair for more details.
Textbook account:
Categories with one object and binary products are studied in:
Aaron Gray and Keith Pardue, Products in a Category with One Object, arXiv:1604.03999 (2016).
Richard Statman, Products in a category with only one object, arXiv:2101.10494 (2021).
Last revised on March 6, 2024 at 17:19:15. See the history of this page for a list of all contributions to it.